Library cyclocevian_conjugate
Require Export PointsType.
Require Import complement.
Require Import isotomic_conjugate.
Require Import isogonal_conjugate.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition cyclocevian_conjugate P :=
isotomic_conjugate
(anticomplement
(isogonal_conjugate
(complement
(isotomic_conjugate P)))).
End Triangle.
Require Import complement.
Require Import isotomic_conjugate.
Require Import isogonal_conjugate.
Open Scope R_scope.
Section Triangle.
Context `{M:triangle_theory}.
Definition cyclocevian_conjugate P :=
isotomic_conjugate
(anticomplement
(isogonal_conjugate
(complement
(isotomic_conjugate P)))).
End Triangle.